open ControlSystem

// Every route is in just one map
assert oneMap {
    all r: Route | one m: Map | r in m.routes
}

check oneMap for 10

assert allNumbersIntoCs{
	all r:Number | r  in getNumbers[]
}

check allNumbersIntoCs for 10

assert allDeviceIsMonitorOrGPS {
	Device = Monitor + GPS
}

check allDeviceIsMonitorOrGPS for 10

assert noTwoBusWithSameGPS {	
	all g1 : GPS | some b : Bus | b.gps = g1
}

check noTwoBusWithSameGPS for 10

assert allBusHasLocation{
		all b:Bus| all t:Time| some l:Location | b.location.t = l
}

check allBusHasLocation for 10
